$\forall$$T$, $A$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $i$:Id, $k$:Knd.
\\[0ex]Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ ($\neg$(locl("a") = $k$))
\\[0ex]$\Rightarrow$ (trigger1\{trigger:ut2, a:ut2, x:ut2\}($T$; $A$; $P$; $i$; $k$) $\in$ Realizer)